가벨향 모 Sanskrit

크�vell~~

o

I'm not going to say sequence, but I'm going to say sequence.

So that you can read it.

So this is our sequence rule for modern logic.

More precisely, not modern.

Why so much German?

Oh, we're talking about it.

Why do the Germans have to steal this?

So this is our sequence rule.

So I don't actually have to wonder whether it's sequence or sequent.

Well, in English it's sequent.

But the actual translation of the German word would be sequent.

Because in the German original text it's actually sekhent, is in sequence.

But the guy who introduced it into English scientific literature probably just politely decreed that the word sequence was already overused in English mathematical texts.

So we prefer the word sequent.

So this is our sequent rule for, well, we wrote box.

And let's introduce an alternative thing for the k to make clear that this rule works for a specific flavor of modal logic namely k, the modal logic of all crypt keyframes.

OK.

We have already seen correctness. Basically that was the last thing we did in last week's Tuesday session.

So it remains to prove completeness.

Completeness in this case isn't going to be terribly hard just as it wasn't terribly hard for the propositional case of which this is an extension.

And that sequence system for k, I mean all the propositional rules plus this one.

If we recall how the propositional case proceeded, this was just via induction on the number of connectives in the sequence in that sense.

And we see here that the same principle with a plot, right?

So the number of connectives decreases going from top to bottom as was there last time already for the Samuels proof which actually used the same principle.

And while I also be a bit careful, this n can be 0.

So as we observe the one connective of which we can be sure that it disappears is this one.

Right. So our eviction is just on the size of the sequence.

So I've said on occasion that every classical proof of completeness would proceed by first reducing the validity of a logical conclusion to unsatisfiability of a set of formulas or some formula.

And then proving that everything that is consistent is satisfied.

Here I would like to deviate from this principle as I think we did for the completeness proof of propositional logic or the sequence calculus for propositional logic.

So we'll just proceed by contraposition.

So we assume that the sequence here, some given sequence, gamma times delta, is not derisable.

And we show that then it is not valid.

So notice that what we prove here is weak completeness.

That is, we take a finite syntactical object, one sequence, and show that it's not derisable.

Stronger proofs of completeness which would actually work for K, but we won't do that here, will actually show satisfiability of infinite consistent sets of formulas,

so they're stronger results.

So we have to do something with our knowledge that the sequence here is not derisable.

Well, not derisable means not derivable by any of the roots.

So we'll now make a distinction on a case distinction on whether or not our target sequence still contains propositional connectives.

So if it still contains a propositional connective somewhere,

then that will be the case that one of the propositional rules applies.

Because the propositional rules are built in such a way that whenever I actually still find a propositional connective somewhere in the sequence, one of the rules will apply.

So I can apply the left negation rule, or if I find a conjunction on the right, I can apply the right conjunction rule. Whatever I find, I can apply a root.

So let's do one example and leave out all the others. That's still the most complicated one.

So let's say we have a right room for conjunction. Let's just say this one. So this room is applicable universal.

But I'll switch the names now if you don't mind. So I'll stick to gamma and delta and just reuse it. I mean, this is all big induction, so this was good level.